ecl-machine2(i;ds;da;x;T;ks;a;upd)
== zupdate-spec-vars(upd).R-state-var(i;ds  x : T;da;z;ds(z);ks;
== zupdate-spec-vars(upd).R-state-var(k,s,v,z'. list_accum(z',nf.nf/n,f.
== zupdate-spec-vars(upd).R-state-var(k,s,v,z'. list_accum(z',nf.if a(n,k,s,v,s(x)) f(s,v)
== zupdate-spec-vars(upd).R-state-var(k,s,v,z'. list_accum(z',nf.else z' fi;
== zupdate-spec-vars(upd).R-state-var(k,s,v,z'. list_accum(z';
== zupdate-spec-vars(upd).R-state-var(k,s,v,z'. list_accum(upd(<k,z>)?nil)) 

latex

---

clarification:

ecl-machine2(i;ds;da;x;T;ks;a;upd)
== zupdate-spec-vars(upd).R-state-var(i;fpf-join(IdDeq;ds;x : T);da;z;fpf-ap(ds; IdDeq; z);ks;
== zupdate-spec-vars(upd).R-state-var(k,s,v,z'.
== zupdate-spec-vars(upd).R-state-var(list_accum(z',nf.nf/n,f.
== zupdate-spec-vars(upd).R-state-var(list_accum(z',nf.if a(n,k,s,v,s(x)) f(s,v) else z' fi;
== zupdate-spec-vars(upd).R-state-var(list_accum(z';
== zupdate-spec-vars(upd).R-state-var(list_accum(fpf-cap(upd;product-deq(Knd;Id;KindDeq;IdDeq);<k
== zupdate-spec-vars(upd).R-state-var(list_accum(fpf-cap(upd;product-deq(Knd;Id;KindDeq;IdDeq);,z>;nil))) 

latex

Definitions	xL.R(x), update-spec-vars(upd), R-state-var(i;ds;da;x;T;ks;tr), f  g, x : v, f(x), x.A(x), list_accum(x,a.f(x;a);y;l), A/x,y. B(x;y), if b t else f fi, f(a), f(x)?z, product-deq(A;B;a;b), Knd, Id, KindDeq, IdDeq, <a,b>, nil
FDL editor aliases	ecl-machine2